1. Field of the Invention
The present invention relates to the design of circuitry. Specifically, the present invention relates to verification of the functionality of the design of logic circuits such as computer systems and integrated circuits.
2. Background Information
One of the problems in modern logic design is the verification that the design actually works in the way it was intended to, according to defined specifications. Various methods include generating software models of the logic circuit design and testing the software model of the design with designer-specified test cases. Because it is not possible to check every possible condition which may be generated in the actual logic design, some of the test cases may not include all of the possible behavior of the logic design, errors may remain because it is not exercised by any of the test cases. Errors in the logic design may remain undetected until the release of a product on the marketplace, when it may cause costly redesigns, and loss of consumer confidence in the product.
An alternative way to check logic design prior to the fabrication of a device is through formal verification. Formal verification is a technique wherein a circuit is modeled as a state transition system, and specifications are provided for components in the system. One way in which specifications may be made is through the use of logic formulas. Each of the components in the logic design is specified, and all possible behaviors of the design may be exercised by a tool which confirms that these specifications are met. Recently, various tools have become available for formal verification such as the Symbolic Model Verification (SMV) software package available from Carnegie-Mellon University, or the COSPAN software package available from Bell Laboratories. These are automatic systems with allow the user to specify the design of the system using software-type commands wherein components in the system are specified by defining input and output signals, and transformation of the signals within each of the components.
Because formal verification exercises all possible behavior of the logic design, and all components in system are defined, this technique has suffered from a deficiency known as "the state explosion problem" due to the very large circuits which are currently being designed. For example, modern microprocessors frequently have more than 3 million transistors. Thus, the number of states which are required to be tested for using formal verification of these circuits are very large indeed and beyond the capabilities of current formal verification techniques.
One way in which such a system may be tested is by reducing the number of states which need to be tested for. One way in which this may be performed is by testing the circuit on a per-property basis. That is, eliminating components (circuitry) and/or signals in a design to reduce the number of states to a number which is able to be performed by current formal verification techniques. A designer could manually eliminate components from a full model and associated circuitry, however, care must be taken that components necessary for testing the desired property are not eliminated. Likewise, the designer may eliminate signals and associated circuitry which are not necessary for testing a desired property. Again, the designer must be careful that associated circuitry which are necessary to test desired properties are not eliminated. Therefore, converting a full model to a reduced model for formal verification poses problems for logic designers.
There is therefore a need to reduce and decompose the model of a circuit down to a size manageable by formal verification tools in a way which maintains that a proof for the properties of a reduced logic model are the same as those for a full logic model from which the reduced model was derived. A need has arisen for tools which assist designers in achieving this goal.